\documentclass[a4paper,10pt]{article}
\usepackage[portuges]{babel}
\usepackage[latin1]{inputenc}

\usepackage{graphicx}
\usepackage{array}
\usepackage{xcolor}
\usepackage{verbatim}
\usepackage{xypic}
\usepackage{pstricks}
\usepackage{vpp}
\usepackage{longtable}
\usepackage{fullpage}
\usepackage{amssymb} 

\definecolor{covered}{rgb}{0,0,0}
\definecolor{not-covered}{gray}{0.5}

\newcommand{\InstVarDef}[1]{{\bf #1}}
\newcommand{\TypeDef}[1]{{\bf #1}}
\newcommand{\TypeOcc}[1]{{\it #1}}
\newcommand{\FuncDef}[1]{{\bf #1}}
\newcommand{\FuncOcc}[1]{#1}
\newcommand{\ClassDef}[1]{{\sf #1}}
\newcommand{\ClassOcc}[1]{#1}

\title{Modela\c{c}\~ao de um Servidor de Publicidade (AdServer) em VDM}
\author{Jo\~ao Paz \and Pedro Ara\'ujo}

\begin{document}

\maketitle

\tableofcontents

\newpage

\section{S\'intese do Problema}

O objectivo \'e modelar um servidor de publicidade (AdServer) e posteriormente testar e validar esse modelo. Um servidor de publicidade (Ad Server), \'e um servidor web que armazena publicidades usadas em campanhas online e entrega as aos visitantes dos websites. A entrega \'e despoletada por um pedido indirecto do visitante ao navegar num website que contenha campanhas publicit\'arias.

A modela\c{c}\~ao ser\'a feita na linguagem VDM, mais precisamente na extens\~ao orientada a objectos VDM++.

Como ponto de partida temos a documenta\c{c}\~ao da modela\c{c}\~ao deste mesmo problema em Alloy e em Java com especifica\c{c}\~oes em JML.

Neste relat\'orio:
\begin{itemize}
 \item Vamos descrever todos os passos de implemeta\c{c}\~ao; 
 \item Vamos mostrar alguns testes realizados bem como a sua cobertura;
 \item Vamos mostrar como tent\'amos validar o modelo;
\end{itemize}

Por fim ser\~ao descritas as dificuldades e conclus\~oes de desenvolvimento. 
 
\newpage

\section{Implementa\c{c}\~ao}

Em VDM++ \'e poss\'ivel ser abstracto, por ser uma extens\~ao de uma linguagem de modela\c{c}\~ao e por outro lado ser concreta (menos abstracta) devido \`a orienta\c{c}\~ao a objectos. Em compara\c{c}\~ao com as abordagens deste problema realizadas anteriormente podemos dizer que a modela\c{c}\~ao em VDM++ fica entre a modela\c{c}\~ao em Alloy  e a de Java, ou seja, nem t\~ao abstracta como Alloy nem t\~ao concreta como Java.
\\
Vamos come\c{c}ar por descrever os tipos e opera\c{c}\~oes das classes utilizadas.\\
Foram criadas duas classes, a classe AdServer e a classe DateUtil. A classe Adserver representa o servidor de publicidade enquanto a classe DateUtil representa a data no calend\'ario gregoriano. A classe Adserver poderia ser desdobrada em mais classes visto existirem v\'arios tipos nela existentes que s\~ao independentes dessa classe. Mas como a modela\c{c}\~ao \'e focada no servidor de publicidade, achamos serem suficiente as duas classes. De seguida para cada classe descrevemos os tipos e respectivos invariantes e opera\c{c}\~oes  juntamente com pr\'e e p\'os condi\c{c}\~oes.

\subsection{AdServer}
A partir da documenta\c{c}\~ao recebida foi bastante simples identificar os tipos desta classe, juntamente com os seus invariantes. Foram identificados os seguintes tipos:
\begin{itemize} 
\item As campanhas;\\
As campanhas s\~ao constitu\'idas pelo seu tipo de campanha, as imagens publicit\'arias (banners), data de in\'icio e fim e frequ\^encia. Existem quatro tipos de campanha: Normal (nenhuma caracter\'istica em especial), Roadblock (todas os espa\c{c}os para publicidade no website s\~ao usadas por imagens de publicidade desta campanha), Sequencing (as imagens de publicidade s\~ao vista por sequ\^encia) e Frequency Capping (a imagem de publicidade s\'o aparece um certo n\'umero de vezes). A frequ\^encia \'e apenas usada para o tipo de campanha Frequency Capping.
\begin{verbatim}
public CampaignType = <NORMAL> | <FREQ_CAP> | <ROAD_BLOCK> | <SEQ>;

public Campaign :: tipo : CampaignType
                   banners : seq of Banner
                   inicio : DateUtil`Date
                   fim : DateUtil`Date
                   freq : nat 

inv c == (c.banners <> [])  and
         (c.tipo = <FREQ_CAP> => c.freq >= 0) and
         (DateUtil`isAfter(c.fim,c.inicio));
\end{verbatim}
Os invariantes apenas indicam que uma campanha deve ter sempre imagens de publicidade; caso seja do tipo Frequency Capping a frequ\^encia n\~ao pode ser menor que zero e a data de fim tem de ser depois da data de in\'icio.
\item Os clientes;\\
Existem dois tipos de clientes, os utilizadores dos websites que ao visitarem um website enviam indirectamente um pedido ao servidor de publicidade e os anunciantes que fazem campanhas de publicidade e as alojam no servidor de publicidade.
\begin{verbatim}
public ClientType = <WEBUSER> | <ADVERTISER>;

public Client :: type : ClientType
              name : seq of char;
\end{verbatim}

\newpage

\item Os websites;\\
Os websites cont\^em os espa\c{c}os/zonas destinados \`a publicidade. O invariante apenas indica que os websites devem ter espa\c{c}os/zonas para publicidade.
\begin{verbatim}
public Website ::  zones : set of Zone
                 url : seq of char
    
inv w == w.zones <> {};
    
public Zone :: id : nat
                x1 : int
                y1 : int;
\end{verbatim}
\end{itemize}
A partir destes tipos podemos descrever agora o servidor de publicidade com:
\begin{itemize}
\item O registo de todos os clientes;
\item O registo de cada campanha;\\
Al\'em da campanha \'e necess\'ario guardar o anunciante e os websites a qual est\'a destinada. 
\begin{verbatim}
public Entry :: client : Client
           campaign : Campaign
           website : set of Website
                
    inv a == a.client.type = <ADVERTISER>;
\end{verbatim}
O invariante indica que o tipo de cliente deve ser do tipo anunciante.
\item A informa\c{c}\~ao relativa \`a vizualiza\c{c}\~ao de imagens de publicidade dos utilizadores;\\
Al\'em do utilizador guarda-se a data do pedido e a imagem pedida ao servidor de publicidade. Assim \'e poss\'ivel ter a informa\c{c}\~ao acerca de que imagens j\'a o utilizador ``viu'' de modo a poder ser geridos os pedidos dos utilizadores de modo a satisfazer as campanhas.
\begin{verbatim}
public ViewInfo :: webuser : Client
              banner : Banner
              date : DateUtil`Date
            
    inv vi == vi.webuser.type = <WEBUSER>;
\end{verbatim}
O invariante indica que o tipo de cliente deve ser do tipo utilizador.
\end{itemize}
Sendo assim, as vari\'aveis de inst\^ancia da classe AdServer s\~ao:
\begin{verbatim}
instance variables

   clientes : set of Client := {};
   campPert : set of Entry := {};
   views : set of ViewInfo := {};
    
   inv invariantes();
\end{verbatim}


Os invariantes destas vari\'aveis de inst\^ancia s\~ao:
\begin{enumerate}
\item Os anunciantes que t\^em campanhas, tamb\'em pertencem aos clientes do servidor de publicidade;
\begin{verbatim}
(forall entry in set campPert & entry.client in set clientes and inv_Entry(entry))
\end{verbatim}
\item O utilizador que fizer um pedido tem de pertencer aos clientes;
\begin{verbatim}
(forall vista in set views & vista.webuser in set clientes and inv_ViewInfo(vista))
\end{verbatim}
\item As imagens de publicidade t\^em de pertencer \`as campanhas;
\begin{verbatim}
forall vista in set views & vista.banner in set dunion 
        ({elems (camp.campaign.banners) | camp in set campPert})
\end{verbatim}
\item Duas campanhas t\^em imagens de publicidade diferentes;
\begin{verbatim}
forall ent1,ent2 in set campPert & ent1<>ent2 => 
   ( {} = (elems (ent1.campaign.banners) inter elems (ent2.campaign.banners)))
\end{verbatim}
\item Para as campanhas do tipo Frequency Capping, o n\'umero de vezes que as imagens foram vistas n\~ao excede o valor freq;
\begin{verbatim}
forall camp in set { camp1 | camp1 in set campPert & camp1.campaign.tipo = <FREQ_CAP>} & 
    card {v.banner | v in set views & v.banner in set elems (camp.campaign.banners) } 
                                <= camp.campaign.freq )
\end{verbatim}
\item Cada website tem no m\'aximo uma campanha de cada anunciante;
\begin{verbatim}
forall ent1,ent2 in set campPert & 
          ent1.client = ent2.client and ent1.campaign <> ent2.campaign => 
                    forall web in set ent1.website & web not in set ent2.website
\end{verbatim}
\item Dois websites t\^em zonas diferentes;
\begin{verbatim}
forall web1,web2 in set dunion { entry.website | entry in set campPert } & 
          web1 <> web2 => ( (web1.zones inter web2.zones) = {} )
\end{verbatim}
\end{enumerate}

Seguem-se as opera\c{c}\~oes desta classe.A opera\c{c}\~ao mais importante \'e a que permite ao utilizador(webuser) pedir uma imagem de publicidade(banner). Esta opera\c{c}\~ao obriga ao servidor de publicidade a gerir as campanhas de modo a satisfazer os anunciantes das campanhas. Por fim existem opera\c{c}\~oes de gest\~ao do registo de clientes e de campanhas.\\
Vamos ver a opera\c{c}\~ao request (pedido), que actualiza o registo das vizualiza\c{c}\~oes do utilizador:
\begin{verbatim}
public request : Zone*Client*DateUtil`Date ==> ()
request(z,c,d) == 
let
    w = getWebsite(z),
    camp = getCamp(w,d),
    b = getBanner(camp)
in 
cases camp.tipo :
    <FREQ_CAP> -> if( getViewsCampaign(camp)<camp.freq ) 
        then views := views union {mk_ViewInfo(c,b,d)}
        else skip,
    <SEQ> -> if ((camp.banners)(len camp.banners) in set { v.banner | v in set views})
        then views := { v | v in set views & v.banner not in set elems camp.banners} union
                {mk_ViewInfo(c,b,d)}
        else views := views union {mk_ViewInfo(c,b,d)},
    <ROAD_BLOCK> -> views := views union { mk_ViewInfo(c,b1,d) | b1 in set elems camp.banners },
    <NORMAL> -> views := views union {mk_ViewInfo(c,b,d)}
end
\end{verbatim}
Em primeiro seleciona-se o website relativo \`a zona, de seguida \'e escolhida a campanha a que a imagem publicit\'aria vai pertencer atrav\'es da opera\c{c}\~ao getCamp(), segue-se a escolha do banner que ser\'a atribu\'ido atrav\'es da opera\c{c}\~ao getBanner() e por fim conforme o tipo da campanha fazer as ac\c{c}\~oes necess\'arias para satisfazer as caracter\'isticas de cada uma. \\

% \newpage

\'E importante destacar o algoritmo da escolha da campanha na opera\c{c}\~ao getCamp(). Nesta opera\c{c}\~ao a escolha de uma campanha \'e feita da seguinte forma:
\begin{itemize}
    \item Reunimos todas as campahas v\'alidas para este website(w) e nesta data(d).
    \item Percorremos cada campanha e, se a campanha f\^or do tipo ROAD\_BLOCK fica essa escolhida, sen\~ao \'e escolhida a campanha com menos visualiza\c{c}\~oes para se manter o equilibrio entre campanhas.
\end{itemize}
O pedido(request) tem  v\'arias pr\'e condi\c{c}\~oes: o cliente que faz o pedido tem de estar registado nos clientes e ser do tipo utilizador e a zona a que se vai atribuir o banner tem de ser de um website que est\'a relacionado com uma campanha.
\begin{verbatim}
pre (c.type = <WEBUSER>) and 
    (c in set clientes) and 
    (z in set dunion { web.zones | web in set dunion { entry.website | entry in set campPert }});
\end{verbatim}
As opera\c{c}\~oes de gest\~ao do registo de clientes e campanhas s\~ao:
\begin{itemize}
\item addClient() que adiciona clientes ao registo de clientes;
\begin{verbatim}
public addClient : Client ==> ()
addClient(cl) == clientes := {cl} union clientes
pre ( cl not in set clientes );
\end{verbatim}
\item addCampaign que adiciona um registo de campanha;
\begin{verbatim}
public addCampaign: Client*Campaign*set of Website ==> ()
addCampaign(cl,c,w) == campPert := {mk_Entry(cl,c,w)} union campPert
pre ( cl.type=<ADVERTISER> and mk_Entry(cl,c,w) not in set campPert );
\end{verbatim}
\end{itemize}

Decidimos n\~ao criar as opera\c{c}\~oes que removem clientes e removem campanhas pois isso obrigaria a remover todas as visualiza\c{c}\~oes por utilizadores e todas as visualiza\c{c}\'oes da campanha removida. Esta opera\c{c}\~ao faria com que o servidor n\~ao conseguisse manter um hist\'orico correcto. Como melhoramento poderia ser implementada uma opera\c{c}\~ao que inutilizasse o cliente mas n\~ao o apagasse do sistema.

\newpage

\subsection{DateUtil}
Esta classe surgiu com a necessidade de ter um tipo de dados que representa-se uma data no calend\'ario gregoriano. Juntamente existem opera\c{c}\~oes que permitem validar e comparar datas.
\begin{verbatim}
public Date :: year : nat
               month: nat
               day  : nat
               hour : nat
               min : nat
  inv d == isValidDate(d.year, d.month, d.day, d.hour, d.min);
\end{verbatim}
O invariante verifica se a data \'e v\'alida atrav\'es da opera\c{c}\~ao isValidDate(). Ainda existem v\'arias opera\c{c}\~oes que auxiliam esta opera\c{c}\~ao.
\begin{verbatim}
public static isValidDate : nat * nat * nat * nat * nat -> bool
isValidDate(year, month, day, hour, min) == 
      year >= 1 and month >= 1 and month <= 12 and 
      day >= 1 and day <= daysOfMonth(year, month) and 
      hour <= 23 and min <= 59;

public static daysOfMonth : nat * nat -> nat
daysOfMonth(year, month) ==
    (cases month :
        1, 3, 5, 7, 8, 10, 12 ->  31,
        4, 6, 9, 11 -> 30,
        2 -> if isLeapYear(year) then 29 else 28
      end)
    pre month >= 1 and month <= 12;
  
public static isLeapYear : nat -> bool
isLeapYear(year) ==
      year mod 4 = 0 and year mod 100 <> 0 or year mod 400 = 0;
\end{verbatim} 
Em rela\c{c}\~ao \`a opera\c{c}\~ao que compara duas datas tem a seguinte estrutura:
\begin{verbatim}
public static isAfter : Date * Date -> bool
    isAfter(d1, d2) ==
      d1.year > d2.year or 
      d1.year = d2.year and d1.month > d2.month or
      d1.year = d2.year and d1.month = d2.month and d1.day > d2.day or 
      d1.year = d2.year and d1.month = d2.month and d1.day = d2.day and d1.hour > d2.hour or
      d1.year = d2.year and d1.month = d2.month and d1.day = d2.day and d1.hour = d2.hour and 
      d1.min > d2.min;
\end{verbatim}

\newpage

\section{Testes}

O pr\'oximo passo \'e o teste das classes AdServer e DateUtil. Foi criada uma classe que contem a bateria de testes. Nessa classe cri\'aram-se v\'arios clientes e campanhas e  fizeram-se v\'arios pedidos. Em seguida, podemos ver um exemplo de uma bateria testes:
\begin{verbatim}
test1: () ==> ()
	test1 () == (
  		dcl cl1 : Adserver`Client := mk_Adserver`Client(<ADVERTISER>,"Pedro");
  		dcl cl2 : Adserver`Client := mk_Adserver`Client(<WEBUSER>,"Paz");
  		dcl cl3 : Adserver`Client := mk_Adserver`Client(<ADVERTISER>,"Ricardo");
  		dcl zone1 : Adserver`Zone := mk_Adserver`Zone(1,1,1,1,1);
  		dcl zone2 : Adserver`Zone := mk_Adserver`Zone(2,2,2,2,2);
  		dcl zone3 : Adserver`Zone := mk_Adserver`Zone(3,3,1,1,1);
  		dcl web1 : Adserver`Website := mk_Adserver`Website({zone1,zone2},"url site1");
  		dcl web2 : Adserver`Website := mk_Adserver`Website({zone3},"url site2");	
  		dcl banner1 : Adserver`Banner := mk_Adserver`Banner(20,20,"banner1");
  		dcl banner2 : Adserver`Banner := mk_Adserver`Banner(20,20,"banner2");
  		dcl banner3 : Adserver`Banner := mk_Adserver`Banner(20,20,"banner3");
  		dcl camp1 : Adserver`Campaign := mk_Adserver`Campaign(<NORMAL>,[banner1],
  		          mk_DateUtil`Date(2008,1,18,23,9),mk_DateUtil`Date(2009,1,18,23,10),0);
  		dcl camp2 : Adserver`Campaign := mk_Adserver`Campaign(<FREQ_CAP>,[banner2],
  		          mk_DateUtil`Date(2008,1,18,23,9),mk_DateUtil`Date(2009,3,18,23,10),1);
  		dcl camp3 : Adserver`Campaign := mk_Adserver`Campaign(<ROAD_BLOCK>,[banner3],
  		          mk_DateUtil`Date(2008,1,18,23,9),mk_DateUtil`Date(2009,1,18,23,10),0);
  		server.addClient(cl1);
  		server.addClient(cl2);
  		server.addClient(cl3);
  		server.addCampaign(cl1,camp1,{web1});
  		server.addCampaign(cl1,camp2,{web2});
  		server.addCampaign(cl3,camp3,{web3});
  		server.request(zone1,cl2,mk_DateUtil`Date(2009,1,18,23,9));
  		server.request(zone3,cl2,mk_DateUtil`Date(2008,10,18,23,9));
  		server.request(zone3,cl2,mk_DateUtil`Date(2008,10,18,23,9));
		);
\end{verbatim}
De seguida com o VDM++ ToolBox foi poss\'ivel saber a cobertura desses mesmos testes, visto que gera o c\'odigo das classe em duas tonalidades, preto caso esteja a ser testado, cinzento caso n\~ao esteja. Tamb\'em gera um quadro que indica a cobertura e o n\'umero de chamadas de cada opera\c{c}\~ao e da cobertura da classe. Tendo essa informa\c{c}\~ao, tent\'amos criar uma bateria de testes cobrisse a totalidade das classe AdServer e DateUtil.\\
Ao tentar cobrir a totalidade do c\'odigo foi poss\'ivel identificar v\'arias falhas, tanto nas opera\c{c}\~oes como nos invariantes. Podemos destacar o caso em que dois websites t\^em a mesma zona, isto n\~ao pode acontecer pois cada website tem as suas pr\'oprias zonas. Com os testes verificamos que n\~ao tinhamos um invariante que garantisse esta propriedade.\\ 
No cap\'tulo 6 e 7, podemos ver o c\'odigo das classes testadas e respectivo quadro com informa\c{c}\~ao da cobertura dos testes realizados. Como \'e poss\'vel verificar consegu\'imos cobrir todo o c\'odigo com os testes realizados.\\
Foi utilizada a API do VDM para Java que tem como finalidade utilizar CORBA para comunicar entre a especifica\c{c}\~ao VDM e o Java para assim ser poss\'ivel fazer testes directamente em Java. Isto n\~ao foi poss\'ivel levar a cabo pois n\~ao conseguimos gerar o ficheiro de refer\^encia vpppref.io que d\'a ao CORBA possibilidade de ``entender'' VDM.
\newpage
\section{Valida\c{c}\~ao}
 
A ideia principal neste fase \'e a valida\c{c}\~ao do c\'odigo criado, ou seja, examinar a integridade das express\~oes usadas. Ap\'os a leitura acerca do tema no manual do utilizador da ferramenta VDMTools foi adquirida alguma informa\c{c}\~ao sobre este tema.

Verificar din\^amicamente os tipos, invariantes, pre e p\'os condi\c{c}\~oes \'e uma forma de teste, como visto no cap\'itulo de Testes, e permite encontrar erros em tempo de execu\c{c}\~ao para espec\'ificos valores de entrada. Enquanto ao examinar a integridade pretendem-se encontrar potenciais erros em tempo de execu\c{c}\~ao.

A VDMTools tem um examinador de integridade que gera propriedades para as opera\c{c}\~oes das classes seleccionadas. A partir das propriedades geradas, a ideia \'e atrav\'es de c\'alculos, caso seja necess\'ario, provar essas propriedades. Se forem alteradas as opera\c{c}\~oes ao tentar satisfazer certas propriedades, s\~ao geradas novas propriedades para serem verificadas.\\
Podemos em seguida mostrar algumas das propriedades geradas e respectivas observa\c{c}\~oes:
\begin{itemize}
\item Na classe AdServer, para a opera\c{c}\~ao getBanner(); 
\begin{verbatim}
(c.banners) <> []
\end{verbatim}
A propriedade gerada indica que a sequ\^encia de banners n\~ao pode ser vazia. Esta propriedade j\'a se verifica devido ao invariante do tipo Campaign, como se pode ver no cap\'itulo 2.1. 
\item Na classe AdServer, para a opera\c{c}\~ao getWebsite();
\begin{verbatim}
(exists1 x in set {web | web in set dunion ({entry.website | entry in set campPert}) & 
z in set web.zones} & z in set x.zones)
\end{verbatim}
Esta propriedade indica para o website ``x'' e zona ``z'' que a opera\c{c}\~ao getWebsite() recebe como argumento:
\begin{itemize}
\item Deve existir um website, no registo das campanhas, que tenha nas suas zonas a zona dada como argumento.
\item A zona deve estar nesse website.
\end{itemize}
Esta propriedade \'e verificada pela pr\'e condi\c{c}\~ao da opera\c{c}\~ao request() que \'e a \'unica que chama a opera\c{c}\~ao getWebsite().
\item Na classe AdServer, para a opera\c{c}\~ao request();
\begin{verbatim}
(len (camp.banners)) in set inds (camp.banners)
\end{verbatim}
Na opera\c{c}\~ao request() (cap\'itulo 2.1) para campanhas do tipo ``Sequencing'' \'e preciso verificar se o \'ultimo banner da sequ\^encia j\'a foi visualizado. Para se obter o \'ultimo banner, vai se \`a posi\c{c}\~ao do tamanho da sequ\^encia. Isto nem sempre \'e poss\'ivel, ou seja, quando a sequ\^encia \'e vazia. Este caso (sequ\^encia vazia) \'e coberto pelo invariante do tipo Campaign (cap\'itulo 2.1).
\item Na classe DateUtil, para a opera\c{c}\~ao daysOfMonth();
\begin{verbatim}
(forall year : nat, month : nat & month >= 1 and month <= 12 =>
 month = (1) or  month = (2) or  month = (3) or  month = (4) or 
 month = (5) or  month = (6) or  month = (7) or  month = (8) or
 month = (9) or month = (10) or month = (11) or month = (12))
\end{verbatim}
Esta propriedade \'e bastante trivial de provar. Para anos e dias maiores que 1 e meses entre 1 e 12 os meses s\'o podem estar entre 1 e 12. A propriedade \'e gerada porque a opera\c{c}\~ao daysOfMonth() (cap\'itulo 2.2) tem um instru\c{c}\~ao case que n\~ao cobre a op\c{c}\~ao ``others''.

\newpage

\item Na classe DateUtil, para a opera\c{c}\~ao isValidDate();
\begin{verbatim}
(forall year : nat, month : nat, day : nat, hour : nat, min : nat &
year >= 1 and month >= 1 and month <= 12 and day >= 1 =>
 DateUtil`pre_daysOfMonth(year, month))
\end{verbatim}
Sabendo que a pr\'e condi\c{c}\~ao da opera\c{c}\~ao daysOfMonth() \'e que o m\^es esteja entre 1 e 12, voltamos a ter uma opera\c{c}\~ao gerada trivial de provar. Esta propriedade \'e gerada porque a opera\c{c}\~ao daysOfMonth() (cap\'itulo 2.2) pode ser chamada sem que se verifique a sua pr\'e condi\c{c}\~ao. N\~ao \'e o caso, visto que antes de se verificar o dia, \'e verificado o m\^es.
\end{itemize}
\newpage

\section{Conclus\~oes/Dificuldades}

Neste projecto a implementa\c{c}\~ao do modelo de um servidor de publicidade foi bastante simples visto j\'a termos a modela\c{c}\~ao deste problema em Alloy. Os testes revelaram-se \'uteis para verificar o comportamento das opera\c{c}\~oes. A valida\c{c}\~ao n\~ao permitiu validar o modelo, ou seja, afirmar que temos 100\% de confian\c{c}a neste modelo, mas conseguimos elevar o n\'ivel de confian\c{c}a ao tentar verificar as propriedades de integridade para as respectivas opera\c{c}\~oes. A pouca informa\c{c}\~ao sobre como utilizar as propriedades de integridade no manual do utilizador da VDMTools tamb\'em nos n\~ao ajudou muito no \^ambito da valida\c{c}\~ao.

A ferramenta VDMTools:
\begin{itemize}
\item A ideia de modelar e em seguida ser gerado c\'odigo java juntamente com os testes \'e bastante interessante.
\end{itemize}
Em contrapartida:
\begin{itemize}
\item N\~ao tem editor de texto
\item O examinador de integridade tem utilidade discut\'ivel visto serem geradas v\'arias propriedades muito abstractas, ou seja, indicam apenas o tipo da propriedade sem mais nenhuma informa\c{c}\~ao.
\end{itemize}

Em suma, a ferramenta VDMTools revelou-se bastante \'util. 

Em rela\c{c}\~ao ao projecto em geral, foi poss\'ivel modelar em VDM um servidor de publicidade, posteriormente realizar testes que cobrissem a totalidade do modelo e por fim tentar aumentar a confian\c{c}a em rela\c{c}\~ao ao modelo atrav\'es da validac{c}\~ao de propriedades.

\newpage

\include{Adserver.vpp}

\include{DateUtil.vpp}

\begin{thebibliography}{10}

\bibitem{Relatorios}
Relat\'orio do Projecto Integrado
\author , Miguel Veiga
\author e Victor Fernandes

\bibitem{Relatorios}
Relat\'orio do Projecto Integrado AdServer especifica\c{c}\~ao em  JML
\author , Miguel Veiga
\author e Victor Fernandes

\bibitem{VDMTools}
The VDM++ Language Manual ver.1.1

\bibitem{VDMTools}
VDMTools User Manual (VDM++) ver.1.2

\bibitem{Livro}
Validated Designs for Object--oriented Systems
\author , John Fitzgerald e Peter Gorm Larsen e Paul Mukherjee e
            Nico Plat e Marcel Verhoef

\end{thebibliography}


\end{document}
